Nuprl Lemma : fpf-empty_wf
11,40
postcript
pdf
A
:Type,
B
:(
A
Type). fpf-empty
fpf(
A
;
x
.
B
(
x
))
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
fpf(
A
;
a
.
B
(
a
))
,
x
(
s
)
,
fpf-empty
,
P
Q
,
prop{i:l}
,
False
,
P
Q
,
guard(
T
)
,
P
Q
Lemmas
it
wf
,
unit
wf
,
l
member
wf
,
nil
member
origin
A:Type, B:(A
Type). fpf-empty 
fpf(A; x.B(x)) A:Type, B:(AType). fpf-empty fpf(A; x.B(x)) x:A. B(x) T
Q
Q
Q